$\forall$$n$, $m$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$$\rightarrow\mathbb{Z}$), $x_{1}$, $x_{2}$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$, $y_{1}$, $y_{2}$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$.
\\[0ex]$\neg$$x_{1}$ $=$ $x_{2}$ $\in$ $\mathbb{Z}$ $\vee$ $\neg$$y_{1}$ $=$ $y_{2}$ $\in$ $\mathbb{Z}$
\\[0ex]$\Rightarrow$ ($\forall$$x$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$, $y$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$. $\neg$($x$ $=$ $x_{1}$ $\in$ $\mathbb{Z}$ \& $y$ $=$ $y_{1}$ $\in$ $\mathbb{Z}$) $\Rightarrow$ $\neg$($x$ $=$ $x_{2}$ $\in$ $\mathbb{Z}$ \& $y$ $=$ $y_{2}$ $\in$ $\mathbb{Z}$) $\Rightarrow$ $f$($x$,$y$) $=$ 0)
\\[0ex]$\Rightarrow$ sum($f$($x$,$y$) $\mid$ $x$ $<$ $n$; $y$ $<$ $m$) $=$ $f$($x_{1}$,$y_{1}$)+$f$($x_{2}$,$y_{2}$)